T:(IdType), tab:secret-table(T). next(tab)  ||tab|| Atom1+Unit 

latex

Definitions	Atom$n, t  T, , {x:A| B(x) }, x:AB(x), x:A. B(x), ||tab|| , #$n, {i..j}, x:AB(x), , inr(x), false, ptr(tab), Unit, left+right, , Type, Prop, True, ij, b, b, s = t, AB, a<b, P  Q, False, A, , T, P & Q, i  j < k, st-atom(tab;n), <a,b>, inl(x), i<j, P  Q, P  Q, next(tab), Id, secret-table(T)
Lemmas	secret-table wf, Id wf, eqtt to assert, assert of lt int, iff transitivity, eqff to assert, squash wf, true wf, bnot of lt int, assert of le int, lt int wf, st-atom wf, unit wf, le wf, bool wf, bnot wf, assert wf, le int wf, st-ptr wf, bfalse wf, it wf, int seg wf, st-length wf, nat wf